Corelab Seminar
2015-2016
Vassilis Zikas
Provable Virus Detection: Using The Observer Effect To Protect Against Malware
Abstract.
Protecting software from malware injection is the holy grail of modern
computer security. Despite intensive efforts by the scientific and
engineering community, the number of successful attacks continues to
increase, making the quest for a solution more pressing than ever. The
problem has attracted little attention in the theoretical computer
science community, where there is even a lack of formal definitions.
In this work we propose a novel provably secure and practically
efficient paradigm for detecting malicious code injection onto a
system's memory. Our system has the following desirable properties: 1)
it protects even systems executing a dynamically updating code; 2) it
requires no changes to the CPU to protect against long continuous
injections, and requires minor changes to the CPU to protect against any
(arbitrary short and scattered) injection attacks that can not read the
code before they inject its software; 3) it only effects the performance
of the program by a modest amount. The first property allows us to
protect both a program and its data without knowing the current state in
the execution (the program might have modified its data while
executing). The second property implies that it can already be used on
today's computers. The third property means that our method is
potentially practical, since performance is critical in most
applications; this is obvious even in its simplified form presented
here, where various optimizations have been avoided for the sake of
clarity in the presentation. Finally, we allow attacks to have both
spatial and temporal freedom: the attack can occur at any time during
the execution and on any part of the memory. It can attack code as well
as data.
Our solutions are accompanied by mathematical proofs that any
injection will be caught with arbitrary high probability. For our
security proofs we provide the first, to our knowledge, formal
cryptographic model tailored to software attestation (detection of
malware injection) in modern computers, which we believe is of
independent interest and paves the way to a thorough theoretical
investigation of the problem.
This is joint work with Richard Lipton and Rafail Ostrovsky.